A:Type, I:MaInterface(A), l:IdLnk, tg:Id, nmr:Namer(2;[tg; lname(l)] @ ma-interface-tags(I)).
Normal(A,I)
 gluable(I;l;tg)
 gluable2(A;I;l;tg)
 (i:Id.
 (i  remove-repeats(IdDeq;ma-interface-locs(I)))
  (if i = source(l)
  (then ma-interface-conds(I;i)
  (else es-in-port-conds(A;(link nmr(0) from i to source(l));nmr(1))
  (fi 
  ( a:Knd fp
  ( V:Type
  (  (State(if ma-interface-loc(I;source(l)) then ma-interface-ds(I;source(l)) else  fi )V
  (  (A + Top)))) 

latex

Definitions

x:A. B(x), P  Q, t  T, if b then t else f fi , tt, ff, A, , x. t(x), , A  B, False, SQType(T), {T}, , State(ds), Top, f(x)?z, x  dom(f), deq-member(eq;x;L), reduce(f;k;as), Y, t.1, , Unit, P  Q, P & Q, x(s), Namer(n;Id_list),

Lemmas

ma-interface-loc wf, lsrc wf, bool wf, eqtt to assert, ma-interface-ds wf, assert-ma-interface-loc, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-empty wf, Id wf, gluable2 wf, gluable wf, ma-interface-normal wf, Namer wf, le wf, append wf, lname wf, ma-interface-tags wf, IdLnk wf, ma-interface wf, member-remove-repeats, Id sq, ma-interface-conds wf3, l member wf, remove-repeats wf, id-deq wf, ma-interface-locs wf, es-in-port-conds wf, mk lnk wf, subtype-fpf2, decl-state wf, top wf, subtype rel product, subtype rel function, subtype rel dep function, fpf-cap wf, subtype rel self, subtype-fpf-cap-top, fpf-empty-sub, eq id wf, assert-eq-id, not functionality wrt iff